\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $L$:(Id List), ${\it del}$:rationals.
\\[0ex]fischer\=\{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2\}\+
\\[0ex](${\it es}$; $L$)
\-\\[0ex]$\Rightarrow$ fischer{-}delay\=\{\=i:l,\+\+
\\[0ex]x:ut2,
\\[0ex]try:ut2,
\\[0ex]taken:ut2,
\\[0ex]contending:ut2,
\\[0ex]free:ut2,
\\[0ex]mine:ut2,
\\[0ex]wanted:ut2,
\\[0ex]z:ut2\}
\-\\[0ex](${\it es}$; ${\it del}$; $L$)
\-\\[0ex]$\Rightarrow$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](loc($e$) $\in$ $L$)
\\[0ex]$\Rightarrow$ @$e$(mkid\{x:ut2\}$\rightarrow$mkid\{free:ut2\})
\\[0ex]$\Rightarrow$ \=($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex]es{-}locl(${\it es}$; $e$; ${\it e'}$)
\\[0ex]$\Rightarrow$ qless(es{-}time(${\it es}$; ${\it e'}$); (es{-}time(${\it es}$; $e$) + ${\it del}$))
\\[0ex]$\Rightarrow$ (es{-}when(${\it es}$; mkid\{x:ut2\}; ${\it e'}$) = mkid\{free:ut2\} $\in$ Id)))
\-\-
\end{tabbing}